Construction sûre de systèmes électroniques
Identifieur interne : 006C82 ( Main/Exploration ); précédent : 006C81; suivant : 006C83Construction sûre de systèmes électroniques
Auteurs : Dominique Cansell [France] ; Stefan Hallerstede ; Yann ZimmermannSource :
- Génie logiciel : (1995) [ 1265-1397 ] ; 2004.
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.
Affiliations:
- France
- Grand Est, Lorraine (région)
- Nancy
- Centre national de la recherche scientifique, Institut national de recherche en informatique et en automatique, Laboratoire lorrain de recherche en informatique et ses applications, Mosel (Loria), Nancy-Université, Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000641
- to stream PascalFrancis, to step Curation: 000400
- to stream PascalFrancis, to step Checkpoint: 000554
- to stream Main, to step Merge: 006F89
- to stream Main, to step Curation: 006C82
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Construction sûre de systèmes électroniques</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Université de Nancy, LORIA</s1><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LORIA</wicri:noRegion><wicri:noRegion>Université de Nancy, LORIA</wicri:noRegion><orgName type="university">Nancy-Université</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Hallerstede, Stefan" sort="Hallerstede, Stefan" uniqKey="Hallerstede S" first="Stefan" last="Hallerstede">Stefan Hallerstede</name><affiliation><inist:fA14 i1="02"><s1>KeesDA</s1><s3>INC</s3><sZ>2 aut.</sZ></inist:fA14><wicri:noCountry>INC</wicri:noCountry></affiliation></author><author><name sortKey="Zimmermann, Yann" sort="Zimmermann, Yann" uniqKey="Zimmermann Y" first="Yann" last="Zimmermann">Yann Zimmermann</name><affiliation><inist:fA14 i1="03"><s1>KeesDA & LDRIA</s1><s3>INC</s3><sZ>3 aut.</sZ></inist:fA14><wicri:noCountry>INC</wicri:noCountry></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">04-0431807</idno><date when="2004">2004</date><idno type="stanalyst">PASCAL 04-0431807 INIST</idno><idno type="RBID">Pascal:04-0431807</idno><idno type="wicri:Area/PascalFrancis/Corpus">000641</idno><idno type="wicri:Area/PascalFrancis/Curation">000400</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000554</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000554</idno><idno type="wicri:doubleKey">1265-1397:2004:Cansell D:construction:sure:de</idno><idno type="wicri:Area/Main/Merge">006F89</idno><idno type="wicri:Area/Main/Curation">006C82</idno><idno type="wicri:Area/Main/Exploration">006C82</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Construction sûre de systèmes électroniques</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>Université de Nancy, LORIA</s1><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>LORIA</wicri:noRegion><wicri:noRegion>Université de Nancy, LORIA</wicri:noRegion><orgName type="university">Nancy-Université</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Hallerstede, Stefan" sort="Hallerstede, Stefan" uniqKey="Hallerstede S" first="Stefan" last="Hallerstede">Stefan Hallerstede</name><affiliation><inist:fA14 i1="02"><s1>KeesDA</s1><s3>INC</s3><sZ>2 aut.</sZ></inist:fA14><wicri:noCountry>INC</wicri:noCountry></affiliation></author><author><name sortKey="Zimmermann, Yann" sort="Zimmermann, Yann" uniqKey="Zimmermann Y" first="Yann" last="Zimmermann">Yann Zimmermann</name><affiliation><inist:fA14 i1="03"><s1>KeesDA & LDRIA</s1><s3>INC</s3><sZ>3 aut.</sZ></inist:fA14><wicri:noCountry>INC</wicri:noCountry></affiliation></author></analytic><series><title level="j" type="main">Génie logiciel : (1995)</title><title level="j" type="abbreviated">Génie logiciel : (1995)</title><idno type="ISSN">1265-1397</idno><imprint><date when="2004">2004</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Génie logiciel : (1995)</title><title level="j" type="abbreviated">Génie logiciel : (1995)</title><idno type="ISSN">1265-1397</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Construction system</term><term>Formal method</term><term>Program verification</term><term>Refinement method</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Méthode formelle</term><term>Vérification programme</term><term>Système construction</term><term>Méthode raffinement</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr">Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li></settlement><orgName><li>Centre national de la recherche scientifique</li><li>Institut national de recherche en informatique et en automatique</li><li>Laboratoire lorrain de recherche en informatique et ses applications</li><li>Mosel (Loria)</li><li>Nancy-Université</li><li>Université de Lorraine</li></orgName></list><tree><noCountry><name sortKey="Hallerstede, Stefan" sort="Hallerstede, Stefan" uniqKey="Hallerstede S" first="Stefan" last="Hallerstede">Stefan Hallerstede</name><name sortKey="Zimmermann, Yann" sort="Zimmermann, Yann" uniqKey="Zimmermann Y" first="Yann" last="Zimmermann">Yann Zimmermann</name></noCountry><country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006C82 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006C82 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:04-0431807
|texte= Construction sûre de systèmes électroniques
}}
| This area was generated with Dilib version V0.6.33. |  |